es:ES, A:Type, X:AbsInterface(A), P:(A), e:E.
((e  X|a.P(a)))  {((e  X)) & (P(X(e)))} 

latex

Definitions

x:A  B(x), P & Q, P  Q, E, x:AB(x), x:A. B(x), , Top, left + right, Type, ES, b, do-apply(f;x), can-apply(f;x), {T}, X(e), e  X, X|a.P(a), AbsInterface(A), t  T, P  Q, s = t, f(a), False, True, P  Q, A, ff, x(s), p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), b, p  q, p  q, p q, tt, , Unit, Void, inr x , <a, b>, let x,y = A in B(x;y), t.1, x:A.B(x), , A c B, outl(x), (x  l)

Lemmas

iff wf, rev implies wf, eqtt to assert, assert wf, not wf, iff transitivity, eqff to assert, assert of bnot, false wf, true wf, event system wf, top wf, bool wf, es-E wf